|
課程名稱 |
自動化軟體驗證
Automatic Verification |
|
開課學期 |
100-2 |
|
授課對象 |
管理學院 資訊管理學研究所 |
|
授課教師 |
蔡益坤 |
|
課號 |
IM7034 |
|
課程識別碼 |
725 M3300 |
|
班次 |
|
|
學分 |
3 |
|
全/半年 |
半年 |
|
必/選修 |
選修 |
|
上課時間 |
星期四6,7,8(13:20~16:20) |
|
上課地點 |
管二204 |
|
備註 |
本課程中文授課,使用英文教科書。
限碩士班以上
總人數上限：30人
外系人數限制：10人 |
|
|
|
|
課程簡介影片 |
|
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
|
課程大綱
|
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
|
課程概述 |
本課程為自動化軟體驗證之入門課程，涵蓋該領域的原理、方法及工具。我們將專注在演算式的方法﹝包括模型檢驗﹞。另一門與本課程互補，名為「軟體規格與驗證」的課程則專注在演譯式的方法﹝包括定理證明﹞。我們將兼顧廣度與深度，不僅研習基礎的原理，也探究一些較成功的方法及工具。 |
|
課程目標 |
使學生熟悉自動化軟體驗證的基礎知識，為未來在該領域從事研究做好準備。 |
|
課程要求 |
本課程包括期末考、數次作業、及一篇期末報告。
每位同學同時必須就一個選定的主題在課堂上做口頭報告，視為期末報告之一部分。
|
|
預期每週課後學習時數 |
|
|
Office Hours |
|
|
指定閱讀 |
|
|
參考書目 |
1. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzmann, Addison-Wesley, 2003.
2. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995.
3. Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008.
|
|
評量方式
(僅供參考) |
|
|